Merge branch 'master' into docs

RedPRL · Mar 20, 2018 · efcaa8d · efcaa8d
2 parents 8c49456 + f4c5ea8
commit efcaa8d
Show file tree

Hide file tree

Showing 21 changed files with 467 additions and 481 deletions.
diff --git a/src/redprl.cm b/src/redprl.cm
@@ -78,18 +78,18 @@ is
   redprl/mini_signature.sig  
 
   redprl/metalanguage/type.sig
+  redprl/metalanguage/syntax.sml
+
   redprl/metalanguage/resolver.sig
-  redprl/metalanguage/syntax.sig
   redprl/metalanguage/elaborate.sig
   redprl/metalanguage/semantics.sig
   redprl/metalanguage/evaluate.sig
 
   redprl/metalanguage/type.sml
   redprl/metalanguage/resolver.fun
-  redprl/metalanguage/syntax.fun
   redprl/metalanguage/elaborate.fun
-  redprl/metalanguage/semantics.fun
-  redprl/metalanguage/evaluate.fun
+  redprl/metalanguage/semantics.sml
+  redprl/metalanguage/evaluate.sml
 
   redprl/signature.sig
   redprl/signature.sml

diff --git a/src/redprl.mlb b/src/redprl.mlb
@@ -88,18 +88,18 @@ in
 
 
     redprl/metalanguage/type.sig
+    redprl/metalanguage/type.sml
+    redprl/metalanguage/syntax.sml
+
     redprl/metalanguage/resolver.sig
-    redprl/metalanguage/syntax.sig
     redprl/metalanguage/elaborate.sig
     redprl/metalanguage/semantics.sig
     redprl/metalanguage/evaluate.sig
 
-    redprl/metalanguage/type.sml
     redprl/metalanguage/resolver.fun
-    redprl/metalanguage/syntax.fun
     redprl/metalanguage/elaborate.fun
-    redprl/metalanguage/semantics.fun
-    redprl/metalanguage/evaluate.fun
+    redprl/metalanguage/semantics.sml
+    redprl/metalanguage/evaluate.sml
 
     redprl/signature.sig
     redprl/signature.sml

diff --git a/src/redprl/machine.fun b/src/redprl/machine.fun
@@ -929,8 +929,8 @@ struct
                                 ty = substVar (s, v) b,
                                 cap = projFromOne s,
                                 tubes =
-                                  [ ((s, Syn.intoDim 0), (w, Syn.into @@ Syn.DIM_APP (Syn.intoSnd (fiberFromOne s), VarKit.toDim w)))
-                                  , ((s, Syn.intoDim 1), (w, projFromOne s)) ]}
+                                  [ ((s, Syn.intoDim 0), (w, Syn.into @@ Syn.DIM_APP (Syn.intoSnd (fiberFromOne (Syn.intoDim 0)), VarKit.toDim w)))
+                                  , ((s, Syn.intoDim 1), (w, coercee)) ]}
                            end
                        in
                          branchOnDim stability syms' (#1 dir)
@@ -1088,14 +1088,50 @@ struct
      | STEP cfg => cfg
      | CRITICAL cfg => cfg
 
+  val ppFrame : frame -> Fpp.doc =
+    fn APP _ => Fpp.text "app"
+     | HCOM _ => Fpp.text "hcom"
+     | COE _ => Fpp.text "coe"
+     | IF _ => Fpp.text "if"
+     | S1_REC _ => Fpp.text "s1-rec"
+     | PUSHOUT_REC _ => Fpp.text "pushout-rec"
+     | COEQUALIZER_REC _ => Fpp.text "coequalizer-rec"
+     | DIM_APP _ => Fpp.text "dim-app"
+     | NAT_REC _ => Fpp.text "nat-rec"
+     | INT_REC _ => Fpp.text "int-rec"
+     | PROJ _ => Fpp.text "proj"
+     | TUPLE_UPDATE _ => Fpp.text "tuple-update"
+     | CAP _ => Fpp.text "cap"
+     | VPROJ _ => Fpp.text "vproj"
+
+  val ppStack : stack -> Fpp.doc = 
+    Fpp.collection (Fpp.text "[") (Fpp.text "]") (Fpp.text ",") o
+      List.map ppFrame
+
+  fun ppCfg (cfg : abt machine) = 
+    let
+      val tm || (_, stk) = cfg
+    in
+      Fpp.grouped @@ Fpp.vsep [TermPrinter.ppTerm tm, Fpp.text "||", ppStack stk]
+    end
+
   fun eval sign stability unfolding = 
     let
       fun go cfg =
         go (unwrapAction (step sign stability unfolding cfg))
-        handle Stuck => cfg
-             | Final => cfg
-             | Neutral _ => cfg 
-             | Unstable => cfg
+        handle Stuck => 
+          let
+            val msg = 
+              Fpp.hvsep
+                [Fpp.text "evaluation got stuck:",
+                 Fpp.align @@ ppCfg cfg]
+          in
+           RedPrlLog.print RedPrlLog.WARN (NONE, msg);
+           cfg
+          end
+          | Final => cfg
+          | Neutral _ => cfg
+          | Unstable => cfg
     in
       unload o go o init
     end