File tree Expand file tree Collapse file tree 2 files changed +1
-31
lines changed Expand file tree Collapse file tree 2 files changed +1
-31
lines changed Original file line number Diff line number Diff line change 5252(show #ineq)
5353<show exec #ineq>
5454
55- 'interactive debugging of execution
56- '(trace #ineq)
57- 
5855'process
5956(:= c (process
6057  (+n0 0)                 'base constellation
6966(show #g)
7067
7168'field access and evaluation
72- (:= (get G X) <eval exec { #G @[(-field X)] }>)
69+ (:= (get G X) << eval exec { #G @[(-field X)] }> >)
7370(show #(get g test1))
7471(show #(get g test2))
7572
8077(:= g2 <eval exec { #g1 @[(-field test1)] }>)
8178<show eval exec { #g2 @[(-field test2)] }>
8279
83- 'extend rays with a head function symbol
84- '<show exec [[(+f X)] [(f X)]][=>+a]>
85- '<show exec [[(+f X)] [(f X)]][=>a]>
86- 
87- 'remove head function symbol from a ray
88- '<show-exec [[(+f X)] [(f X)]][+f=>]>
89- 
90- 'substitutions
91- '<show exec (+f X)[X=>(+a X)]>
92- '<show exec (+f X)[+f=>+g]>
93- '<show exec (union #1 #2)
94- '  [#1=>[(+f X) X)]]
95- '  [#2=>(-f a)]>
96- 
9780'define type
9881(spec nat {
9982  [(-nat 0) ok]
Original file line number Diff line number Diff line change 11open  Base 
2- open  Out_channel 
3- open  In_channel 
42
53let  ( let* )  x  f  =  Result. bind x ~f 
64
@@ -160,7 +158,6 @@ let string_of_ban = function
160158let  string_of_star  s  = 
161159  match  s.content with 
162160  |  []  -> " []" 
163-   |  [ r ] -> string_of_ray r
164161  |  _  ->
165162    Printf. sprintf " [%s%s]" 
166163      (List. map ~f: string_of_ray s.content |>  String. concat ~sep: "  " 
@@ -293,11 +290,6 @@ let fusion repl1 repl2 s1 s2 bans1 bans2 theta : star =
293290  ; bans =  List. map (nbans1 @  nbans2) ~f: (fmap_ban ~f: (subst theta))
294291  }
295292
296- let  pause  ()  = 
297-   flush stdout;
298-   let  _ =  input_line stdin in 
299-   () 
300- 
301293let  group_bans = 
302294  List. fold_left ~init: ([] , [] ) ~f: (function  ineq , incomp  -> 
303295    (function 
@@ -414,11 +406,6 @@ let rec select_star ~linear ~queue actions :
414406    |  Some  new_stars , new_actions  ->
415407      (Some  (List. rev queue @  other_states @  new_stars), new_actions) )
416408
417- let  string_of_cfg  (actions , states ) : string  = 
418-   Printf. sprintf " >> actions: %s\n >> states: %s\n " 
419-     (string_of_constellation actions)
420-     (string_of_constellation states)
421- 
422409let  exec  ?(linear  = false )  mcs  : constellation  = 
423410  (*  do a sequence of rounds with a single interaction on state per round *) 
424411  let  rec  loop  (actions , states ) = 
 
 
   
 
     
   
   
          
    
    
     
    
      
     
     
    You can’t perform that action at this time.
  
 
    
  
    
      
        
     
       
      
     
   
 
    
    
  
 
  
 
     
    
0 commit comments